Nuprl Definition : grp_leq
13,42
postcript
pdf
a
b
==
(
a
b
)
latex
clarification:
a
g
b
==
(
a
(
g
)
b
)
latex
Up
groups
1
Wellformedness Lemmas
grp
leq
wf
Definitions
b
,
x
f
y
,
origin
b == 
(a 
b)
g b == (a (g) b) b == (a b)
g b == (a (g) b) b